Inference at * 2 1 1 
Iof proof for Lemma fseg select:



1. T : Type
2. l1 : T List
3. l2 : T List
4. ||l1||  ||l2||
5. i:. (i < ||l1||)  (l1[i] = l2[((||l2|| - ||l1||)+i)])
  l2 = (firstn(||l2|| - ||l1||;l2) @ l1) 

latex

 by Assert l1 = nth_tl(||l2|| - ||l1||;l2)  

latex

 1: .....assertion..... NILNIL

 1:   l1 = nth_tl(||l2|| - ||l1||;l2)
 2: 

 2: 6. l1 = nth_tl(||l2|| - ||l1||;l2)
 2:   l2 = (firstn(||l2|| - ||l1||;l2) @ l1)
 .

Definitions

s = t, type List, nth_tl(n;as), n - m, ||as||